T:Type, L1, L2:(T List), a, b, c:T.
no_repeats(T;L2)
 L1  L2
 adjacent(T;L1;a;b)
 adjacent(T;L2;a;c)
 (c before b  L2  (b = c)) 

latex

Definitions	L1  L2, no_repeats(T;l), adjacent(T;L;x;y), x before y  l, left + right, P  Q, x:AB(x), P  Q, x:A. B(x), s = t, Type, type List
Lemmas	no repeats wf, sublist wf, adjacent wf, l before wf, adjacent-sublist, before-adjacent2